Homotopy Type Theory(HoTT)
ホモトピー型理論(Homotopy Type Theory; HoTT)
Martin-Löf型理論とホモトピー理論を融合させたイメージ？
HoTTが出てきた背景としては、現代の数学は検証するのがとても難しくなっていて、誤りが含まれると誤りが累積してしまい、後続の証明が全て誤りになって困るという問題がある
人力で検証するには現代数学は大きくなりすぎた
HoTTの基本的なアイディアは、型を空間、要素を点と解釈すること
計算機科学の型理論における「＝」を, 位相幾何学のホモトピー同値「連続変形がある」の性質で解釈しようとする試み 型 = 論理 = 集合 = 圏論 = ホモトピーの対応がある
構成される理論にHoTTがあると計算機上でよりうまく証明ができるようになる？
含まれているもの
理解するためには色々見る
$ a : A
$ A は空間で、$ a は空間の点
$ f: A → B
$ A → B
$ x: A
$ x は型$ A の変数(variable)
$ U は型の型(宇宙と呼ばれる)
型、論理、集合、ホモトピーの対応はHoTTの本に書いてあった。翻訳したものは下記。
$ \begin{array}{c|c|c|c} 型(\mathrm{Types}) & 論理(\mathrm{Logic}) & 集合(\mathrm{Sets}) & ホモトピー \\ \hline A & 命題 & 集合 & 空間 \\ a: A & 証明 & 元 & 点 \\ B(x) & 述語 & 集合の族 & ファイブレーション \\ b(x) : B(x) & \mathrm{条件付き証明} & 元の族 & \mathrm{切断} \\ \bm{0, 1} & \bot , \top & \varnothing , \{ \varnothing \} & \varnothing, * \\ A + B & A \lor B & \mathrm{非交和} & 余直積 \\ A \times B & A \land B & 組の集合 & 積の空間 \\ A \to B & A \implies B & 関数の集合 & 関数空間 \\ \sum_{(x:A)}B(x) & \exist_{x:A} B(x) & \mathrm{直和} & \mathrm{全空間} \\ \prod_{(x:A)}B(x) & \forall_{x:A} B(x) & 積 & 切断の空間 \\ \mathrm{Id}_A & 等号\ = & \lbrace (x, x) | x \in A \rbrace & 道空間A^I \end{array}
ref: "Homotopy Type Theory Univalent Foundations of Mathematics" Table 1: Comparing points of view on type-thoretic operations (P11)
Lean 2時点はHoTTを理論通りに実装することができず、Lean 3でHoTTのサポートを切ったという経緯がある 今はLean 4でHoTTの実装をしようとしている人がいる
確認用
Q. Homotopy Type Theory(HoTT)とは
Q. 型理論とは
Q. Martin-Löf型理論とは
Q. HoTTを学ぶと何がうれしいか
参考
動画
Felix Cherubini, A foundation for synthetic algebraic geometry - YouTube
https://www.youtube.com/watch?v=lp4kcmQ0ueY
関連